00100		The problem is formulated in FOL by asserting the sentences
00200	
00300		A = '((1 BN 6)(1 WP 1 WP 2 WP 1)(2 BP 4 X)(2 BP 5)(BP 2 BP 4)
00400			(BP BK 1 WR BP 1 BP)(2 BN WR 3 WK)),
00500	
00600		chesslegal(P),
00700	
00800		board(P) = subst(X,'X,A),
00900	
01000	and
01100	
01200		¬(X='B).
01300	
01400	It is then required to prove from the above and the axioms of chess
01500	and using the chess eye that X = 'WB.
01600	
01700		Herein the side of the first equation is a description of a
01800	chess board with an unknown piece, the second statement asserts that
01900	a certain position arose in a legal game and has its board the expression
02000	A with something called X substituted for the atomic symbol X.
02100	The last statement asserts that X is not the symbol B standing for
02200	a blank square.  
02300	
02400		We are making a distinction between a position and a board, and
02500	this distinction appears to be necessary to formulate the problem in
02600	a compact way.  A position determines a board but also includes whose
02700	move it is, and information necessary to determine which pieces can
02800	participate in castling, which pawn if any may be taken en passant,
02900	and even how many times the board has been repeated and how far along
03000	we are to the fifty moves.  For the purpose of fairy chess additional
03100	information may be necessary, e.g. one may be asked in the given postion
03200	where a piece came from.  Perhaps the simplest way of handling the matter
03300	is to make the position identical with the complete sequence of moves
03400	from the beginning of the game.
03500	
03600	
03700	The Chess Eye:
03800	
03900		In the informal solution of the problem, a great role is played
04000	by the human ability to answer certain questions about chess situations
04100	without reasoning.  For example, it is directly observable that Black
04200	is in check in P.  The Chess Eye in FOL will be a set of functions and
04300	predicates that can directly answer those questions without reasoning.
04400	This is accomplished by attaching certain predicate and function symbols
04500	to LISP functions that generate certain sentences by simplification
04600	without reasoning.  Thus we would like to generate a sentence saying
04700	that the WR on his K7 checks the black king.
04800	
04900		However, there are some problems in specifying what the chess
05000	eye looks at.  The obvious thing is to say that it looks at positions,
05100	but this won't work in the present case without excessive work, because
05200	the board is not completely given: there are a priori 12 possible boards
05300	corresponding to the different values of X, and the board doesn't specify
05400	the position, since we don't know what piece the rook at WK8 is; in fact
05500	it is WKBP.
05600	
05700		Therefore, it turns out that the chess eye should operate on
05800	\F1partial boards\F0.  The relevant partial board for determining that
05900	Black is in check is given by the S-expression
06000	
06100		B = '( 6 ((8 U)) (U BK 1 WR (4 U)) ((8 U))).
06200	
06300	which specifies only the black king, the white rook and the empty square
06400	in between.  From this partial board it follows that Black is in check
06500	and that therefore it is White's move.  There is a partial ordering of
06600	partial boards in terms of amount of specification, and there is a
06700	chess eye predicate that can immediately decide this ordering.  Moreover,
06800	there is a chess eye predicate that can be asked whether
06900	one piece checks another in a partial board.  It can assert the proposition,
07000	assert its negation, or fail to make an assertion according to which
07100	way the proposition is decided by the partial board or whether the
07200	board is too partial to decide.
07300	
07400		That Black is in check is obtained from FOL by first giving the
07500	command
07600	
07700		simplify seecheck('B,63,B);
07800	
07900	which returns
08000	
08100		seecheck('B,63,B)
08200	
08300	as a new statement, because the SEECHECK LISP function to which \F1seecheck\F0
08400	has been attached can make that computation directly.
08500	The meaning of the assertion is that Black is in check from square 63 (6 is
08600	the rank measured from 0 to 7 and 3 is the file) in the partial board B.
08700	To repeat the point, giving this help  is considered merely providing
08800	FOL what every chess player can see from the situation.  
08900	
09000		Next we define the partial board
09100	
09200		A1 = '((1 BN 6)(1 WP 1 WP 2 WP 1)(2 BP 4 U)(2 BP 5)(BP 2 BP 4)
09300			(BP BK 1 WR BP 1 BP)(2 BN WR 3 WK)),
09400	
09500	which has an ambiguity only at WQR4.
09600	
09700		simplify part(B,A1);
09800	
09900	yields the statement
10000	
10100		part(B,A1)
10200	
10300	because the predicate \F1part\F0 is attached to a LISP function PART that
10400	can tell whether one partial board is part of another.
10500	
10600	*******
10700	
10800	Note: It would be even better if there were a FOL macro or
10900	step generator that could accept a command
11000	
11100		do check(B)
11200	
11300	and would then define new INDCONSTs \F1a\F0 and \F1b\F0 and
11400	generate the conjunction
11500	
11600		checks(a,b,B) ∧ location(a,B) = 63 ∧ value(a,B) = 'WR ∧
11700	location(b,B) = 61 ∧ value(b,B) = 'BK.
11800	
11900	The \F1do\F0 command would operate the proof generator \F1check\F0.
12000	A \F1proof generator\F0 can do arbitrary computations with its
12100	arguments which lead to certain FOL commands being generated.
12200	These commands are then submitted  \F1do\F0 to FOL and if
12300	FOL likes them, they are executed.  If FOL doesn't like one,
12400	the proof generator can either give up in disgust or try to
12500	generate something else.  After it is through generating steps
12600	it may edit some of them away in order not to leave statements
12700	around that are purely internal to its reasoning.  In the present
12800	case, the generator \F1check\F0 would examine the board B for
12900	checks.  If it didn't find any, it would call the \F1simplify\F0
13000	command with an appropriate Chess Eye function that would generate
13100	an assertion to that effect.  If it found a check, it would call
13200	\F1seecheck\F0 with arguments that were determined by its
13300	search of the board, and then it would generate further FOL steps
13400	to deduce the desired conjunction.  In the present case, the
13500	\F1check\F0 proof generator would save only a little effort,
13600	but it seems to me that our huan ability to identify the
13700	checks on the board corresponds to the existence of this
13800	generator.  In other words, when one human tells another
13900	to look at the checks at the beginning of his argument
14000	about what the last move was, I claim he is providing
14100	the call on the \F1check\F0 generator and no additional
14200	information.
14300	
14400		Anyway, we all have previously discussed adding
14500	something like proof generators to FOL
14600	
14700	******* (end of te)
     

00100	
00200		Our next goal is the statement
00300	
00400		∀ X.(